(declare-const outerObj Null?)
(declare-const id Type?)
(push)
(assert (not (= outerObj ObjNull)))
(assert (not (= id TypeNull)))
(assert (str.in.re (value1 id) (re.+ (re.range "\x20" "\x7e"))))
(assert (str.contains (value1 (Type (str.++ (value1 (Type "prefix of" 0)) (value1 id)) (value2 id))) (value1 (Type "something" 27))))
(check-sat)
(pop)
(push)
(assert (not (= id TypeNull)))
(assert (str.in.re (value1 id) (re.+ (re.range "\x20" "\x7e"))))
(assert (str.contains (value1 (Type (str.++ (value1 (Type "prefix of" 0)) (value1 id)) (value2 id))) (value1 (Type "something" 27))))
(check-sat)
(pop)
(push)
(assert (not (= id TypeNull)))
(assert (str.in.re (value1 id) (re.+ (re.range "\x20" "\x7e"))))
(assert (str.contains (value1 (Type (str.++ (value1 (Type "prefix of" 0)) (value1 id)) (value2 id))) (value1 (Type "something" 27))))
(check-sat)
(pop)
(push)
(assert (not (= id TypeNull)))
(assert (str.in.re (value1 id) (re.+ (re.range "\x20" "\x7e"))))
(assert (str.contains (value1 (Type (str.++ (value1 (Type "prefix of" 0)) (value1 id)) (value2 id))) (value1 (Type "something" 27))))
(check-sat)
(pop)
(push)
(assert (not (= outerObj ObjNull)))
(assert (not (= id TypeNull)))
(assert (str.in.re (value1 id) (re.+ (re.range "\x20" "\x7e"))))
(assert (str.contains (value1 (Type (str.++ (value1 (Type "prefix" 0)) (value1 id)) (value2 id))) (value1 (Type "something" 27))))
(check-sat)
(pop)
(push)
(assert (not (= id TypeNull)))
(assert (str.in.re (value1 id) (re.+ (re.range "\x20" "\x7e"))))
(assert (str.contains (value1 (Type (str.++ (value1 (Type "prefix" 0)) (value1 id)) (value2 id))) (value1 (Type "something" 27))))
(check-sat)
(pop)
